tactic =df step --> step

Any unary function denoted by a symbol in *tactics* is a tactic.
Let (F X) be any application where F is a symbol in *tactics*
and (fun F) : (A --> B) and X : A then (F X) is a tactic


Let (F X1 ... Xn) be any application of the type (list sequent)
then if F is an element of *tactics* then (F X1 ... Xn) is a step

For a given A1 ... An, let (fn F) be of the type A1 .... An --> (list sequent) --> (list sequent)
then if F is an element of *tactics* then (fn F) is of the type A1 .... An --> step --> step.


if (element? F (value *tactics*))
(fn F) : (list sequent) --> (list sequent);
__________________________________
(fn F) : (step --> step);

if (element? F (value *tactics*))
(fn F) : (A --> (list sequent) --> (list sequent));
__________________________________
(fn F) : (A --> step --> step);

if (element? F (value *tactics*))
(fn F) : (A --> B --> (list sequent) --> (list sequent));
__________________________________
(fn F) : (A --> B --> step --> step);


(datatype tactics

  F : tactic;
  (F X) : (list sequent);
  _______________
  (F X) : step;

  if (element? F (value *tactics*))
  _________________________________
  F : tactic;

  F : tactic;
  _______________
  (F X) : tactic;
  
  X : step;
  _________
  X : (list sequent);)